   \appendix
   %%
   % Intro CPN
   %
   \chapter{Introdução à Modelagem e Simulação com Redes de Petri Coloridas}
   \label{app:apendice-cpn}

   Uma rede CPN é uma classe de redes de petri com recursos para definição e manipulação
de tipos de dados denominados "cores", possibilitando adicionar semântica aos modelos. Em
termos de modelagem isso significa que as marcações podem representar estruturas de dados
tal como em ambientes de programação. As cores de um modelo CPN são declaradas através
de uma linguagem funcional chamada CPN-ML.

   As seções a seguir apresentam uma introdução ao formalismo de uma rede CPN, um exemplo
didático de modelagem, o simulador para análise de desempenho e o relatório de espaço de
estado, visando auxiliar o leitor no entendimento da estratégia de modelagem utilizada
neste trabalho.

   \section{Definição Formal}

      Formalmente, uma rede de petri colorida é uma tupla $CPN = \\ (P, T, A,\sum, V, C,
G, E, I)$, onde:

   \begin{enumerate}
    \item $P$ um conjunto finito de \textbf{lugares}
    
    \item $T$ é um conjunto finito de \textbf{transições} $T$ tal que $P \cap T =
\emptyset$.

    \item $A \subset P \times T \cup T \times P$ é um conjunto de \textbf{arcos}
direcionados.
    
    \item $\sum$ é um conjunto finito não-vazio de \textbf{cores}.
    
    \item $V$ é um conjunto finito de \textbf{variáveis tipadas} tal que $Type[v] \in
\sum$ para todas as variáveis $v \in V$.

    \item $C:P \rightarrow \sum$ é uma \textbf{função de cores} que associa uma
\textbf{cor}  a cada um dos \textbf{lugares}.

     \item $G:T \rightarrow EXPRv$ é uma \textbf{função de guarda} que associa a cada $t
\in T$ uma expressão tal que $Type[G(t)] = Bool$.

     \item $E:A \rightarrow EXPRv$ é uma \textbf{função de anotação de arco} que associa
uma expressão a cada $a \in A$ tal que $Type[E(a)]=C(p)ms$, onde $p$ é o \textbf{lugar}
conectado ao \textbf{arco} $a$.

     \item $I:P \rightarrow\ EXPR\emptyset$ é uma \textbf{função de inicialização} que
associa a cada $p \in P$ uma expressão tal que $Type[I(p)]=C(p)ms$.
   \end{enumerate}

 
    Uma rede de petri colorida com temporização adiciona os seguintes conceitos
    :
    \begin{itemize}
     \item Uma marcação é uma função $M$ que mapeia cada lugar $p \in P$ em um conjunto 
$M(p)$ de marcações tal que
      $M(p) \in C(p)_{MS}$ se $p$ não é temporizado;
      
      $M(p) \in C(p)_{TMS}$ se $p$ é temporizado;
      
     \item Uma \textbf{marcação temporizada} é um par $(M,t^*)$, onde $M$ é uma marcação
e $t^* \in \mathbb{T}$ é o valor do relógio global do modelo.

     \item A \textbf{marcação temporizada inicial} é o par $(M_0,0)$, onde $M_0$
é definido por $M_0(p) = I(p) \langle\rangle$ para todo $p \in P$.
    \end{itemize}
   
   
   \section{Exemplo de Modelo CPN }

      O modelo apresentado na Figura \ref{fig:cpn-exemplo} foi adotado para explicar
as características e a notação utilizada em modelagem baseada em redes de petri
coloridas. O modelo ilustra um cenário simples de atendimento ao cidadão para retirada
de documentos tipo RG, CPF e CNH. Para ser atendido, a pessoa deve aguardar em uma fila
de triagem, onde será identificado o tipo de serviço e então, se encaminhar para uma sala
de espera. Para os serviços de RG e CPF, as pessoas serão encaminhadas para um grupo de
atendentes, e o serviço de CNH para outro grupo de atendentes. A triagem conta com duas
atendentes, o serviço de RG/CPF conta com três atendentes e o serviço de CNH conta com
duas atendentes.

    \begin{sidewaysfigure}
    \centering
    \includegraphics[scale=0.65]{figuras/exemplo-didatico.png}
    \caption{Modelo CPN Exemplo}
    \label{fig:cpn-exemplo}
    \end{sidewaysfigure}

      A Figura \ref{fig:cpn-exemplo} ilustra o ambiente CPN Tool com a área de modelagem,
as declarações e as ferramentas de simulação. 

      Observando as declarações do modelo, é possível notar a existência das cores
\texttt{SERVICO} e \texttt{PESSOA}. A cor \texttt{SERVICO} define os tipos de serviços
prestados (CHN, RG e CPF) através da declaração \texttt{with}. Fazendo um paralelo a uma
linguagem de programação, é o equivalente a utilizar enumerações, ou seja, os valores
possíveis são previamente definidos. A cor \texttt{PESSOA} é o produto das cores INT e
SERVICO. Novamente fazendo um paralelo a uma linguagem de programação, é o equivalente ás
\textit{structs} da linguagem C.


      No modelo CPN é possível observar o lugar \texttt{Fila Atendimento}, com a indicação
\texttt{PESSOA} no lado inferior direito. Isso significa que as marcações nesse lugar
serão do tipo \texttt{PESSOA}. Adicionalmente, o lugar \texttt{Fila Atendimento} inicia
com uma marcação onde o serviço a ser solicitado é o \texttt{CNH}. Observa-se isso pela
inscrição \texttt{1`(1,CNH)}.

      Cada tipo de atendimento está representado no modelo por um lugar, são eles, 
\texttt{Atend Triagem}, \texttt{Atend RG CPF} e \texttt{Atend CNH}. Para modelar o número
de atendentes, cada um dos lugares representando um tipo de atendente tem um outro lugar
com o número de atendentes disponíveis, são eles, \texttt{Triagem Disponivel},
\texttt{Atend RG CPF Disp} e \texttt{Atend CNH Disp}. As marcações iniciais em cada um
deles representam a quantidade de atendentes disponíveis.

      A transição \texttt{atender RG CPF} possui a guarda \texttt{[servico=RG orelse
servico=CPF]}, e a transição \texttt{atender CHN} possui a guarda \texttt{[servico=CNH]}.
Isso indica que essas transições só serão habilitadas quando o valor da variável
\texttt{servico} das marcações existentes no lugar \texttt{Sala Espera} obedecerem à
condição declarada nas respectivas guardas. Adicionalmente, a transição \texttt{atender
RG CPF} possui uma marcação de tempo \texttt{@+30}, e a transição \texttt{atender CHN}
possui a marcação de tempo \texttt{@+50}. Esse tipo de inscrição na transição representa
o tempo gasto para que uma pessoa seja atendida, 30 unidades de tempo para RG/CPF e 50
unidades de tempo para CNH.  O mesmo pode ser observado na inscrição
\texttt{(i,servico)@++10} do arco que conecta a transição \texttt{passar triagem} ao lugar
\texttt{Atend Triagem}. Nesse caso, o atendimento na triagem demora 10 unidades de tempo.

      Por fim, a inscrição \texttt{chegada(i)@+10} no arco que conecta a transição
\texttt{passar triagem} ao lugar \texttt{Fila Atendimento} indica que a cada disparo
dessa transição a função \texttt{chegada(i)} será executada. A função, por sua vez, em
cada execução gera uma marcação no lugar \texttt{Fila Atendimento} respeitando o tipo
PESSOA, ou seja, uma marcação no formato \texttt{1`(1,CNH)}, onde o valor CNH, RG ou CPF
é gerado aleatoriamente obedecendo uma distribuição uniforme, observado no código CPN-ML
da função pela linha \texttt{val tipoServico = uniform(0.0,1.0)}. A função
\texttt{uniform(Real,Real)} é uma função pré-definida da linguagem CPN-ML, que no exemplo,
irá gerar valores uniformemente distribuídos entre \texttt{0.0} e \texttt{1.0}.


      Mesmo com um exemplo simples, é possível notar o potencial da ferramenta para
simular sistemas complexos, pois combina as características do formalismo das redes de
petri, com o poder de representatividade da linguagem funcional CPN-ML.

      
   \section{Simulação e Ferramentas de Análise}

   \subsection{Espaço de Estado}

      Um espaço de estados é um grafo $G = (V, E)$, tal que $V$ é o conjunto de vértices,
representando o conjunto de marcações alcançáveis, e $E$ é o conjunto de arestas
rotuladas, representando o conjunto de transições. 

      A partir do grafo de espaço de estados, pode-se analisar diversas propriedades
comportamentais, tais como a inexistência de \textit{deadlock}, alcançabilidade de uma
marcação específica, contorno limitado e marcação de origem. Adicionalmente, a ferramenta
gera um grafo conectado - \textit{Strongly-Connected-Component Graph} (SCC)

   \subsection{Análise de Desempenho}

      A análise de desempenho é conduzida através de sucessivas execuções de um modelo
CPN temporizado. Para simular chegada de requisições (carga), normalmente utiliza-se um
módulo específico onde uma função associada a um arco indica o intervalo entre cada
requisição, conforme utilizado no modelo para a arquitetura baseada em espaço de tuplas,
observado na Figura \ref{fig-cpn-arrival}.

      As demais marcações de tempo de um modelo podem indicar atrasos, tempos de
processamento em recursos específicos, \textit{timeout}, entre outros. A base de tempo
utilizada pelo simulador é o chamado \textit{Model Time}, ou seja, o tempo global do
simular que inicia-se em \texttt{0} e é incrementado com base nas definições de tempo
utilizadas nas inscrições dos arcos ou nas transições, conforme ilustrado no modelo
exemplo.


      As métricas de desempenho são obtidas através de coletas de dados durante as
simulações. Em modelos CPN, a coleta de dados é realizada através de monitores
denominados \textit{Data Collection Monitors}, os quais podem ser definidos para cada
medida de desempenho de interesse. 

      Um monitor inclui uma função de predicado (\textit{predicate function}), que
determina quando o dado deve ser coletado, e uma função de observação (\textit{observation
function}) que determina qual dado deve ser coletado. 

%       No exemplo a seguir, utilizado neste trabalho, a função de predicado retorna
% \texttt{true} quando a variável \texttt{resp} é igual a \texttt{r200} e a variável
% \texttt{req} igual a \texttt{ACK}, ou seja, só será coletado quando houver uma
% resposta de sucesso e a requisição SIP for do tipo ACK. 
% 
%       Quando executada, a função de observação irá retornar a diferença entre o tempo
% global do modelo no momento da execução (\textit{ModelTime}) representado pela função
% \texttt{time()} e o valor da variável \texttt{toa} que no modelo indica o tempo em que a
% requisição entrou no sistema (\textit{Time-Of-Arrival}).
% 
%    \begin{verbatim}
%    fun pred (Devices_Node1'Receive_Response (1, 
%       {auth,finish,n,node,req,resp,sop,toa})) = 
%            (resp=r200 andalso req=ACK)
%          | pred _ = false
% 
%    fun obs (Devices_Node1'Receive_Response (1, 
%       {auth,finish,n,node,req,resp,sop,toa})) = 
%         ModelTime.sub(time(),ModelTime.fromInt(toa))
%       | obs _ = 0.0
%    \end{verbatim}

      As funções de monitoração são escritas em linguagem CPN-ML. No
Apêndice \ref{app:apendice-monitores} são apresentadas as funções de monitoração
utilizadas para coleta de dados neste trabalho. Adicionalmente, a ferramenta de modelagem
permite a utilização de monitores pré-definidos, sem a necessidade de escrever código
CPN-ML.



   %%
   % Funções de monitoração
   %
   \chapter{Funções de Monitoração e Coleta de Dados}\label{app:apendice-monitores}

      Conforme já mencionado anteriormente, o simulador CPN Tool permite a criação de
monitores para coleta de dados de simulação utilizando-se "\textit{Data Collector
Monitoring Functions}", as quais apresentam um alto grau de flexibilidade, uma vez que as
funções são escritas em código CPN-ML para atender necessidades específicas. 

      Este apêndice apresenta o código-fonte CPN-ML das funções de coleta de
dados utilizadas para extração de resultados da simulação da arquitetura baseada em espaço
de tuplas.

   \begin{description}
      \item[AvgTupleDTS], responsável pela coleta da média de tuplas no DTS.
   
\begin{verbatim}
   fun pred (bindelem,
            P2P'DTS_1_mark : TUPLE tms,
            Server_Node1'B_1_mark : TUPLE tms,
            Server_Node2'D_1_mark : TUPLE tms,
            Server_Node3'E_1_mark : TUPLE tms,
            Server_Node4'H_1_mark : TUPLE tms) = 
      let
         fun predBindElem (Server_Node1'in_DTS(1,
            {auth,finish,i,n,node,req,resp,sop,toa})) = true
          | predBindElem (Server_Node2'in_DTS (1,
            {auth,finish,i,n,node,req,resp,sop,toa})) = true
          | predBindElem (Server_Node3'in_DTS (1, 
            {auth,finish,i,n,node,req,resp,sop,toa})) = true
          | predBindElem (Server_Node4'in_DTS (1, 
            {auth,finish,i,n,node,req,resp,sop,toa})) = true
          | predBindElem _ = false
      in
         predBindElem bindelem  
      end

   fun obs (bindelem,
            P2P'DTS_1_mark : TUPLE tms,
            Server_Node1'B_1_mark : TUPLE tms,
            Server_Node2'D_1_mark : TUPLE tms,
            Server_Node3'E_1_mark : TUPLE tms,
            Server_Node4'H_1_mark : TUPLE tms) = 
      let
         val tDTS = (size P2P'DTS_1_mark)
         val tB = (size Server_Node1'B_1_mark)
         val tD = (size Server_Node2'D_1_mark)
         val tE = (size Server_Node3'E_1_mark)
         val tH = (size Server_Node4'H_1_mark)
         val total = tDTS + tB+tD+tE+tH+1
         fun obsBindElem (Server_Node1'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = total
            | obsBindElem (Server_Node2'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = total
            |obsBindElem (Server_Node3'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = total
            | obsBindElem (Server_Node4'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = total
            | obsBindElem _ = 0
      in
         obsBindElem bindelem  
      end
\end{verbatim}

   \item[WaitingTimeDTS], responsável pela coleta da média de tempo de permanência de
tuplas no DTS. 
   \begin{verbatim}
   fun pred (bindelem) = 
      let
         fun predBindElem (Server_Node1'in_DTS (1,
             {auth,finish,i,n,node,req,resp,sop,toa})) = true
            | predBindElem (Server_Node2'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = true
            | predBindElem (Server_Node3'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = true
            | predBindElem (Server_Node4'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = true
            | predBindElem _ = false
      in
         predBindElem bindelem  
      end

   fun obs (bindelem) = 
      let
         fun obsBindElem (Server_Node1'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = 
                 Real.fromInt(IntTime() - sop)
            | obsBindElem (Server_Node2'in_DTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = 
                 Real.fromInt(IntTime() - sop)
            | obsBindElem (Server_Node3'in_DTS (1,
             {auth,finish,i,n,node,req,resp,sop,toa})) = 
                 Real.fromInt(IntTime() - sop)
            | obsBindElem (Server_Node4'in_DTS (1,
             {auth,finish,i,n,node,req,resp,sop,toa})) = 
                 Real.fromInt(IntTime() - sop)
            | obsBindElem _ = 0.0
      in
            obsBindElem bindelem  
      end
   \end{verbatim}
   
   \item[AvgTuplesLTS], responsável pela coleta da média tuplas no LTS.
   \begin{verbatim}
   fun pred (bindelem,
              LTS_Node1'LTS_Node1_1_mark : TUPLE tms,
              LTS_Node1'N1_C_1_mark : TUPLE tms,
              LTS_Node1'N1_E_1_mark : TUPLE tms) = 
      let
         fun predBindElem (LTS_Node1'outC (1, 
             {auth,finish,n,node,req,resp,sop,toa})) = true
            | predBindElem (LTS_Node1'outS (1, 
             {auth,finish,n,node,req,resp,sop,toa})) = true
            | predBindElem _ = false
      in
         predBindElem bindelem  
      end

   fun obs (bindelem,
              LTS_Node1'LTS_Node1_1_mark : TUPLE tms,
              LTS_Node1'N1_C_1_mark : TUPLE tms,
              LTS_Node1'N1_E_1_mark : TUPLE tms) = 
      let
         val tLTS = (size LTS_Node1'LTS_Node1_1_mark)
         val tN1C = (size LTS_Node1'N1_C_1_mark)
         val tN1E = (size LTS_Node1'N1_E_1_mark)
         val total = tLTS + tN1C + tN1E
         fun obsBindElem (LTS_Node1'outC (1, 
             {auth,finish,n,node,req,resp,sop,toa})) = total
            | obsBindElem (LTS_Node1'outS (1, 
             {auth,finish,n,node,req,resp,sop,toa})) = total
            | obsBindElem _ = 0
      in
         obsBindElem bindelem  
      end
   \end{verbatim}
   
   \item [WaitingTimeLTS], responsável pela coleta do tempo médio de permanência de
tuplas no LTS. 
   \begin{verbatim}
   fun pred (bindelem) = 
      let
         fun predBindElem (Server_Node1'in_LTS (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = true
            | predBindElem _ = false
      in
         predBindElem bindelem  
      end

   fun obs (bindelem) = 
      let
         fun obsBindElem (Server_Node1'in_LTS (1, 
          {auth,finish,i,n,node,req,resp,sop,toa})) = 
               Real.fromInt(IntTime() - sop)
         | obsBindElem _ = 0.0
      in
         obsBindElem bindelem  
      end
   \end{verbatim}
   
   \item [LoadCSCF], responsável pela coleta da ocupação média do componente CSCF.
   \begin{verbatim}
   fun pred (bindelem,
              Server_Node1'CSCF_1_mark : TUPLE tms,
              Server_Node1'INV_1_mark : TUPLE tms,
              Server_Node1'REG_1_mark : TUPLE tms) = 
      let
         fun predBindElem (Server_Node1'Process_Tuple (1, 
             {auth,finish,i,n,node,req,resp,sop,toa})) = true
            | predBindElem _ = false
      in
         predBindElem bindelem  
      end

   fun obs (bindelem,
              Server_Node1'CSCF_1_mark : TUPLE tms,
              Server_Node1'INV_1_mark : TUPLE tms,
              Server_Node1'REG_1_mark : TUPLE tms) = 
      let
         val tcscf = (size Server_Node1'CSCF_1_mark)
         val tinv = (size Server_Node1'INV_1_mark)
         val treg = (size Server_Node1'REG_1_mark)
         fun obsBindElem (Server_Node1'Process_Tuple (1, 
               {auth,finish,i,n,node,req,resp,sop,toa})) = 
              tcscf + tinv + treg
            | obsBindElem _ = 0
      in
         obsBindElem bindelem  
      end
   \end{verbatim}
   
   \item [SessionSetupDelay], responsável pela coleta do tempo médio gasto nas operações
de início de sessão. 
   \begin{verbatim}
   fun pred (Devices_Node1'Receive_Response (1, 
      {auth,finish,n,node,req,resp,sop,toa})) = 
           (resp=r200 andalso req=ACK)
         | pred _ = false

   fun obs (Devices_Node1'Receive_Response (1, 
      {auth,finish,n,node,req,resp,sop,toa})) = 
        ModelTime.sub(time(),ModelTime.fromInt(toa))
      | obs _ = 0.0
   \end{verbatim}

   \item [RegistrationDelay], responsável pela coleta do tempo médio gasto nas operações
de registro. 
   \begin{verbatim}
   fun pred (Devices_Node1'Receive_Response (1, 
      {auth,finish,n,node,req,resp,sop,toa})) = 
        (resp=r200 andalso req=REGISTER)
      | pred _ = false

   fun obs (Devices_Node1'Receive_Response (1, 
      {auth,finish,n,node,req,resp,sop,toa})) = 
        ModelTime.sub(time(),ModelTime.fromInt(toa))
      | obs _ = 0.0
\end{verbatim} 

\end{description}

   %%
   % Modelo CPN IMS padrao
   %
   \chapter{Modelo CPN para Arquitetura IMS padrão}\label{app:apendice-modelo-cpn-default}

    A Figura \ref{fig:cpn-rede-default} apresenta o modelo CPN para a arquitetura IMS
padrão, tradicionalmente utilizada para implantar redes IMS.

    O modelo considera a existência de três servidores, cada um representando uma
entidade funcional do CSCF, e a comunicação entre essas entidades. Importante observar
que o modelo utilizou as mesmas funções de temporização empregadas no modelo CPN da
arquitetura baseada em espaço de tuplas.

  \begin{sidewaysfigure}[ht]
    \centering
    \includegraphics[scale=0.5]{figuras/fig-cpn-rede-default.png}
    \caption{Modelo CPN para a Arquitetura IMS padrão}
    \label{fig:cpn-rede-default}
  \end{sidewaysfigure}  
  